\begin{tabbing}
ecl{-}trans{-}act(${\it ds}$; ${\it da}$; $A$)($n$,$L$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List\+
\\[0ex]$\exists$\=${\it tr}$:event{-}info(${\it ds}$;${\it da}$)\+
\\[0ex](($L$ = append(${\it L'}$; cons(${\it tr}$; [])) $\in$ (event{-}info(${\it ds}$;${\it da}$) List))
\\[0ex]$\wedge$ spreadn(\=${\it tr}$;\+
\\[0ex]$k$,$s$,$v$.(($k$ $\in$ ecl{-}trans{-}ks($A$) $\in$ Knd)
\\[0ex]c$\wedge$ ($\uparrow$(ecl{-}trans{-}a($A$)($n$,$k$,$s$,$v$,ecl{-}trans{-}state($A$; ${\it L'}$)))))))
\-\-\-
\end{tabbing}